COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	prolog.not[w82,jmc]	Notes on control in logic programming
C00004 00003	The need to represent prolog states.
C00006 ENDMK
C⊗;
prolog.not[w82,jmc]	Notes on control in logic programming

Predicate Logic as a Computational Formalism, Keith L. Clark

Problem: develop a program that can solve the eight queens problem
without knowing in advance that there can be only one queen in
each row and column.  It should deduce this fact and only then
choose an appropriate representation for the heuristic search.
Only this would be an honest solution of the eight queens problem.

← Queen_sol(1.2. ... .8.nil,y)

	Queen_sol(x,y) ← Perm(x,y) & Safe(y)

We have

	Perm(Nil,Nil) ←

	Perm(u.x, v.z) ← delete(v, u.x, y) ∧ Perm(y, z)

where

	delete(u, u.x, x) ←

	delete(u, v.x, v.z) ← delete(u, x, z).

The  Safe  relation is given by

	Safe(Nil) ←

	Safe(u.x) ← no_take(u, x, 1) ∧ Safe(x)

where

	no_take(u, Nil, n) ←

	no_take(u, v.x, n) ← no_diagonal(u, v, n) ∧ no_take(u, x, s(n))

and

	no_diagonal(u, v, n) ← v > u ∧ v = u+w ∧ w ≠ n

	no_diagonal(u, v, n) ←  u > v  ∧ u = v+w ∧ w ≠ n
The need to represent prolog states.

	In Lisp, we can represent partial evaluation states by expressions.
Thus we can write

(A B)*(C D) = if n (A B) then (C D) else [a(A B)].d(A B)*(C D)
		= A.[(D)*(C D)]
		= etc.

	We need to be able to do the same in prolog or other logic
programming languages.  Such a state might be representable as a
clause or assertion or set of clauses.

	Meta-rules need to be able to make logic preserving transformations
of logic programs, e.g. re-ordering of goals in a clause, before doing
substantive computations.
However, it looks like we need to be able to do such transformations,
especially re-ordering, in the middle of the execution of the program.

	In some sense macros are a kind of meta-computation.  The parallel
would be closer if there were some specialized meaning preserving
operations to make macros out of.


Lisp and prolog

	Lisp definitions can be used in the same way as prolog statements
by a suitable Lisp inference machine.  For example if we have

u*v = if null u then v else [a u].[d u * v],

then we can try to solve equations like

u*(A B) = v

etc., just as in prolog.